XL-2: a match arm keeps its own refusal cause in every arm position; the value reader carries the fold's refusal - #12321

What

v2 body lowering now keeps a match arm's own refusal cause in every arm position. It no longer re-reads a refused arm under the wrong shape and reports body_lowering_reason_match_arm_navigation_refused, which carried the arm as its only locus.

XL-2 fold cleanup, item (1) (the fall-back reader). Owner: quiet-seal-543.

The chain, and where it first went wrong

I bisected dag/gunbc/accelerator_demo/accelerator_demo_eval.dag down to its smallest refusing shape. The refusal is not specific to lists, nesting or if: a refusable value in any match arm after the first (or in a comma-separated arm) refuses as navigation. The same value in the first arm refuses located. I tagged each of the 14 body_lower_match_arm_navigation_reject callers to find the one that fires. The earliest unjustified link was one step above the arm wiring:

• body_lower_extract_comma_list_arm_head, the earliest wrong link. It wired the node as an arm and, on any Rejected, discarded the diagnostics and retried the same node as a comma-repeat element. An arm that refused for its own located cause was re-read under the wrong shape, and the retry answered navigation. Repair: decide the shape first, then wire once, and let Rejected stand. A repeat element is Seq(optional-comma, arm), so its left side is a separator, as body_lower_match_arm_repeat_elem_is_separator already decides; an arm's left side is its pattern, which never is. body_lower_match_arm_from_comma_repeat_elem is deleted: it had no other caller.
• body_lower_value_lowered, the brief's link. When the bottom-up fold refused, it handed the raw value to the top-down walker, discarding the fold's cause. It now carries the fold's Rejected.
• One arm-body reader. The sequence arm path read bodies through body_lower_value_lowered, but the two spine arm paths used the operand reader alone. All three now go through body_lower_match_arm_wired (value reader first, its Rejected carried; the operand reader only when it answers Absent). This is §3: one question, one authority.

Witness

v2.test.claim.namespace_xl0.match_arm_refusal_carried covers five inline modules through the native front end. Each is judged by the fatal cause of its file refusal.

Both sides were run with local claim_batch, same binary, with only the fold file swapped. Each claim costs about 1.48M eval steps, almost all of it the shared front end, so marc_outcomes is enrolled WARM in v2.workflow.floor_pure_producer_share, as iasl_outcomes is.

Why the claims are relational. The specimen is a list literal, the shape the corpus specimen refused on. The claims do not name body_lowering_reason_list_literal_unlowered, because #12208 deletes that cause when it lowers lists. They assert instead that arm position does not change the cause. If a later change lowers the specimen, a_first_arm_specimen_still_refuses_located goes red by name and the specimen value is replaced, rather than three accepts greening the relational claims.

Identity census (main 69e0bb7566e vs head 7692619dc7a, the fold change alone)

Instrument: native_test_context_from_ingest file_refusals, one ingest per path, head_reason and fatal_reason. It ran remotely in batches of 25, same binary on both sides, with only the checkout differing. Coverage so far is PARTIAL: 1,000 of 6,778 .dag files under dag/ and src/v2/ are paired. The rest is running in waves against BuildBuddy's 1-hour cap, and the full table will be posted as a PR comment. Hand-off to the parent waits on the full census; the PR is marked ready now only so CI and the floor can plan the witness in parallel.

27 of the 1,000 paired files change. No file goes from refused on main to accepted on head.

Not in this PR (so this PR is not read as closing them)

• Arms 3+ of a match are dropped silently (gentle-crane-869, about 457 atoms). This is the next PR in this lane, in the same reader. v2.test.claim.body_lowering.single_arm_match pins that drop today.
• body_lower_find_control_form_optional (a record, call or binary expression containing a block lowers to the block alone) is not touched here. It is a separate queue item.
• An as-cast operand is accepted in every arm position on both sides, which means it is carried, not refused. That is item (4)'s evidence, recorded here.

Carrier wording (for compiler_frontend_program_status, not edited here)

v2 body lowering keeps a refused match arm's own cause and locus in every arm position (body_lower_extract_comma_list_arm_head decides the arm shape before wiring and never discards an arm's Rejected), and body_lower_value_lowered carries a fold refusal instead of re-reading the value through the walker. Witness: v2.test.claim.namespace_xl0.match_arm_refusal_carried.

Stage0

No generated stage0 file derives from the changed functions, so none is installed.

Other

The census ran with a per-batch child cgroup memory.max bound after the build, not GUNBC_MEMORY_BUDGET_BYTES. The parent agreed: the budget variable is the refusal-bypass DESIGN §5 forbids. No catch-all binder arm over an Rc-held coproduct was added, so the known read.clone() E0308 emitter defect is not exercised.

🤖 Generated with Claude Code